\begin{tabbing}
$\forall$$x_{1}$:es\_realizer\{i:l\}. 
\\[0ex]($\uparrow$Reffect?($x_{1}$))
\\[0ex]$\Rightarrow$ (\=Reffect{-}f($x_{1}$)\+
\\[0ex]$\in$ (\=(decl{-}state(Reffect{-}ds($x_{1}$))$\rightarrow$Reffect{-}T($x_{1}$)$\rightarrow$decl{-}type\=\{i:l\}\+\+
\\[0ex](\=Reffect{-}ds($x_{1}$); Reffect{-}x($x_{1}$)\+
\\[0ex])) + (decl{-}state(\=Reffect{-}ds\+
\\[0ex]($x_{1}$))
\-\-\-\\[0ex]$\rightarrow$Reffect{-}T($x_{1}$)$\rightarrow$rationals$\rightarrow$decl{-}type\=\{i:l\}\+
\\[0ex](Reffect{-}ds($x_{1}$); Reffect{-}x($x_{1}$)))))
\-\-\-
\end{tabbing}